0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 187 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 204 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 25 ms)
↳13 QDP
↳14 UsableRulesReductionPairsProof (⇔, 131 ms)
↳15 QDP
↳16 QDPSizeChangeProof (⇔, 0 ms)
↳17 YES
↳18 PiDP
↳19 UsableRulesProof (⇔, 0 ms)
↳20 PiDP
↳21 PiDPToQDPProof (⇒, 0 ms)
↳22 QDP
↳23 UsableRulesReductionPairsProof (⇔, 128 ms)
↳24 QDP
↳25 PisEmptyProof (⇔, 0 ms)
↳26 YES
countD_in_ga(atom(T4), s(0)) → countD_out_ga(atom(T4), s(0))
countD_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countD_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countD_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_ga(T8, T29, T30, T32, countD_in_ga(T30, T32))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U8_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, X60)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_ga(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
countD_in_ga(cons(cons(T157, T158), T159), T150) → U11_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
U11_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, X247)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
countD_in_ga(cons(cons(T157, T158), T159), T150) → U12_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_ga(T157, T158, T159, T150, countD_in_ga(T160, T150))
U13_ga(T157, T158, T159, T150, countD_out_ga(T160, T150)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
U10_ga(T8, T51, T52, T53, T55, countD_out_ga(T56, T55)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U7_ga(T8, T29, T30, T32, countD_out_ga(T30, T32)) → countD_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
countD_in_ga(atom(T4), s(0)) → countD_out_ga(atom(T4), s(0))
countD_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countD_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countD_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_ga(T8, T29, T30, T32, countD_in_ga(T30, T32))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U8_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, X60)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_ga(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
countD_in_ga(cons(cons(T157, T158), T159), T150) → U11_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
U11_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, X247)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
countD_in_ga(cons(cons(T157, T158), T159), T150) → U12_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_ga(T157, T158, T159, T150, countD_in_ga(T160, T150))
U13_ga(T157, T158, T159, T150, countD_out_ga(T160, T150)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
U10_ga(T8, T51, T52, T53, T55, countD_out_ga(T56, T55)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U7_ga(T8, T29, T30, T32, countD_out_ga(T30, T32)) → countD_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_GA(T8, T29, T30, T32, countD_in_ga(T30, T32))
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTD_IN_GA(T30, T32)
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_GA(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → FLATTENC_IN_GGGA(T51, T52, T53, X60)
FLATTENC_IN_GGGA(T63, T64, T65, X85) → U6_GGGA(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
FLATTENC_IN_GGGA(T63, T64, T65, X85) → FLATTENB_IN_GGGA(T63, T64, T65, X85)
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_GGGA(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTENA_IN_GA(T90, X131)
FLATTENA_IN_GA(cons(atom(T106), T107), .(T106, X158)) → U1_GA(T106, T107, X158, flattenA_in_ga(T107, X158))
FLATTENA_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTENA_IN_GA(T107, X158)
FLATTENA_IN_GA(cons(cons(T116, T117), T118), X175) → U2_GA(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
FLATTENA_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENB_IN_GGGA(T116, T117, T118, X175)
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_GGGA(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENB_IN_GGGA(T125, T126, T127, X192)
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139, X209) → U5_GGGA(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENB_IN_GGGA(T136, T137, cons(T138, T139), X209)
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_GA(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_GA(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_GA(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
U9_GA(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → COUNTD_IN_GA(T56, T55)
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → U11_GA(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → FLATTENB_IN_GGGA(T157, T158, T159, X247)
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → U12_GA(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_GA(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_GA(T157, T158, T159, T150, countD_in_ga(T160, T150))
U12_GA(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → COUNTD_IN_GA(T160, T150)
countD_in_ga(atom(T4), s(0)) → countD_out_ga(atom(T4), s(0))
countD_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countD_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countD_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_ga(T8, T29, T30, T32, countD_in_ga(T30, T32))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U8_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, X60)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_ga(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
countD_in_ga(cons(cons(T157, T158), T159), T150) → U11_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
U11_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, X247)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
countD_in_ga(cons(cons(T157, T158), T159), T150) → U12_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_ga(T157, T158, T159, T150, countD_in_ga(T160, T150))
U13_ga(T157, T158, T159, T150, countD_out_ga(T160, T150)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
U10_ga(T8, T51, T52, T53, T55, countD_out_ga(T56, T55)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U7_ga(T8, T29, T30, T32, countD_out_ga(T30, T32)) → countD_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_GA(T8, T29, T30, T32, countD_in_ga(T30, T32))
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTD_IN_GA(T30, T32)
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_GA(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → FLATTENC_IN_GGGA(T51, T52, T53, X60)
FLATTENC_IN_GGGA(T63, T64, T65, X85) → U6_GGGA(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
FLATTENC_IN_GGGA(T63, T64, T65, X85) → FLATTENB_IN_GGGA(T63, T64, T65, X85)
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_GGGA(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTENA_IN_GA(T90, X131)
FLATTENA_IN_GA(cons(atom(T106), T107), .(T106, X158)) → U1_GA(T106, T107, X158, flattenA_in_ga(T107, X158))
FLATTENA_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTENA_IN_GA(T107, X158)
FLATTENA_IN_GA(cons(cons(T116, T117), T118), X175) → U2_GA(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
FLATTENA_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENB_IN_GGGA(T116, T117, T118, X175)
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_GGGA(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENB_IN_GGGA(T125, T126, T127, X192)
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139, X209) → U5_GGGA(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENB_IN_GGGA(T136, T137, cons(T138, T139), X209)
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_GA(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_GA(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_GA(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
U9_GA(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → COUNTD_IN_GA(T56, T55)
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → U11_GA(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → FLATTENB_IN_GGGA(T157, T158, T159, X247)
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → U12_GA(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_GA(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_GA(T157, T158, T159, T150, countD_in_ga(T160, T150))
U12_GA(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → COUNTD_IN_GA(T160, T150)
countD_in_ga(atom(T4), s(0)) → countD_out_ga(atom(T4), s(0))
countD_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countD_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countD_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_ga(T8, T29, T30, T32, countD_in_ga(T30, T32))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U8_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, X60)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_ga(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
countD_in_ga(cons(cons(T157, T158), T159), T150) → U11_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
U11_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, X247)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
countD_in_ga(cons(cons(T157, T158), T159), T150) → U12_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_ga(T157, T158, T159, T150, countD_in_ga(T160, T150))
U13_ga(T157, T158, T159, T150, countD_out_ga(T160, T150)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
U10_ga(T8, T51, T52, T53, T55, countD_out_ga(T56, T55)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U7_ga(T8, T29, T30, T32, countD_out_ga(T30, T32)) → countD_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTENA_IN_GA(T90, X131)
FLATTENA_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTENA_IN_GA(T107, X158)
FLATTENA_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENB_IN_GGGA(T116, T117, T118, X175)
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENB_IN_GGGA(T125, T126, T127, X192)
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENB_IN_GGGA(T136, T137, cons(T138, T139), X209)
countD_in_ga(atom(T4), s(0)) → countD_out_ga(atom(T4), s(0))
countD_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countD_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countD_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_ga(T8, T29, T30, T32, countD_in_ga(T30, T32))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U8_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, X60)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_ga(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
countD_in_ga(cons(cons(T157, T158), T159), T150) → U11_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
U11_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, X247)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
countD_in_ga(cons(cons(T157, T158), T159), T150) → U12_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_ga(T157, T158, T159, T150, countD_in_ga(T160, T150))
U13_ga(T157, T158, T159, T150, countD_out_ga(T160, T150)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
U10_ga(T8, T51, T52, T53, T55, countD_out_ga(T56, T55)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U7_ga(T8, T29, T30, T32, countD_out_ga(T30, T32)) → countD_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTENA_IN_GA(T90, X131)
FLATTENA_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTENA_IN_GA(T107, X158)
FLATTENA_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENB_IN_GGGA(T116, T117, T118, X175)
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENB_IN_GGGA(T125, T126, T127, X192)
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENB_IN_GGGA(T136, T137, cons(T138, T139), X209)
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90) → FLATTENA_IN_GA(T90)
FLATTENA_IN_GA(cons(atom(T106), T107)) → FLATTENA_IN_GA(T107)
FLATTENA_IN_GA(cons(cons(T116, T117), T118)) → FLATTENB_IN_GGGA(T116, T117, T118)
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127) → FLATTENB_IN_GGGA(T125, T126, T127)
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139) → FLATTENB_IN_GGGA(T136, T137, cons(T138, T139))
No rules are removed from R.
FLATTENB_IN_GGGA(atom(T78), atom(T89), T90) → FLATTENA_IN_GA(T90)
FLATTENA_IN_GA(cons(atom(T106), T107)) → FLATTENA_IN_GA(T107)
FLATTENA_IN_GA(cons(cons(T116, T117), T118)) → FLATTENB_IN_GGGA(T116, T117, T118)
FLATTENB_IN_GGGA(atom(T78), cons(T125, T126), T127) → FLATTENB_IN_GGGA(T125, T126, T127)
POL(FLATTENA_IN_GA(x1)) = 1 + 2·x1
POL(FLATTENB_IN_GGGA(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3
POL(atom(x1)) = 1 + x1
POL(cons(x1, x2)) = x1 + x2
FLATTENB_IN_GGGA(cons(T136, T137), T138, T139) → FLATTENB_IN_GGGA(T136, T137, cons(T138, T139))
From the DPs we obtained the following set of size-change graphs:
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_GA(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_GA(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → COUNTD_IN_GA(T56, T55)
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTD_IN_GA(T30, T32)
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → U12_GA(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_GA(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → COUNTD_IN_GA(T160, T150)
countD_in_ga(atom(T4), s(0)) → countD_out_ga(atom(T4), s(0))
countD_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countD_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countD_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U7_ga(T8, T29, T30, T32, countD_in_ga(T30, T32))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U8_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, X60))
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U8_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, X60)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
countD_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_ga(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_ga(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → U10_ga(T8, T51, T52, T53, T55, countD_in_ga(T56, T55))
countD_in_ga(cons(cons(T157, T158), T159), T150) → U11_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, X247))
U11_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, X247)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
countD_in_ga(cons(cons(T157, T158), T159), T150) → U12_ga(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_ga(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → U13_ga(T157, T158, T159, T150, countD_in_ga(T160, T150))
U13_ga(T157, T158, T159, T150, countD_out_ga(T160, T150)) → countD_out_ga(cons(cons(T157, T158), T159), T150)
U10_ga(T8, T51, T52, T53, T55, countD_out_ga(T56, T55)) → countD_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U7_ga(T8, T29, T30, T32, countD_out_ga(T30, T32)) → countD_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U9_GA(T8, T51, T52, T53, T55, flattenC_in_ggga(T51, T52, T53, T56))
U9_GA(T8, T51, T52, T53, T55, flattenC_out_ggga(T51, T52, T53, T56)) → COUNTD_IN_GA(T56, T55)
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTD_IN_GA(T30, T32)
COUNTD_IN_GA(cons(cons(T157, T158), T159), T150) → U12_GA(T157, T158, T159, T150, flattenB_in_ggga(T157, T158, T159, T160))
U12_GA(T157, T158, T159, T150, flattenB_out_ggga(T157, T158, T159, T160)) → COUNTD_IN_GA(T160, T150)
flattenC_in_ggga(T63, T64, T65, X85) → U6_ggga(T63, T64, T65, X85, flattenB_in_ggga(T63, T64, T65, X85))
flattenB_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U3_ggga(T78, T89, T90, X131, flattenA_in_ga(T90, X131))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U4_ggga(T78, T125, T126, T127, X192, flattenB_in_ggga(T125, T126, T127, X192))
flattenB_in_ggga(cons(T136, T137), T138, T139, X209) → U5_ggga(T136, T137, T138, T139, X209, flattenB_in_ggga(T136, T137, cons(T138, T139), X209))
U6_ggga(T63, T64, T65, X85, flattenB_out_ggga(T63, T64, T65, X85)) → flattenC_out_ggga(T63, T64, T65, X85)
U3_ggga(T78, T89, T90, X131, flattenA_out_ga(T90, X131)) → flattenB_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U4_ggga(T78, T125, T126, T127, X192, flattenB_out_ggga(T125, T126, T127, X192)) → flattenB_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U5_ggga(T136, T137, T138, T139, X209, flattenB_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenB_out_ggga(cons(T136, T137), T138, T139, X209)
flattenA_in_ga(atom(T97), .(T97, [])) → flattenA_out_ga(atom(T97), .(T97, []))
flattenA_in_ga(cons(atom(T106), T107), .(T106, X158)) → U1_ga(T106, T107, X158, flattenA_in_ga(T107, X158))
flattenA_in_ga(cons(cons(T116, T117), T118), X175) → U2_ga(T116, T117, T118, X175, flattenB_in_ggga(T116, T117, T118, X175))
U1_ga(T106, T107, X158, flattenA_out_ga(T107, X158)) → flattenA_out_ga(cons(atom(T106), T107), .(T106, X158))
U2_ga(T116, T117, T118, X175, flattenB_out_ggga(T116, T117, T118, X175)) → flattenA_out_ga(cons(cons(T116, T117), T118), X175)
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → U9_GA(flattenC_in_ggga(T51, T52, T53))
U9_GA(flattenC_out_ggga(T56)) → COUNTD_IN_GA(T56)
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTD_IN_GA(T30)
COUNTD_IN_GA(cons(cons(T157, T158), T159)) → U12_GA(flattenB_in_ggga(T157, T158, T159))
U12_GA(flattenB_out_ggga(T160)) → COUNTD_IN_GA(T160)
flattenC_in_ggga(T63, T64, T65) → U6_ggga(flattenB_in_ggga(T63, T64, T65))
flattenB_in_ggga(atom(T78), atom(T89), T90) → U3_ggga(T78, T89, flattenA_in_ga(T90))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127) → U4_ggga(T78, flattenB_in_ggga(T125, T126, T127))
flattenB_in_ggga(cons(T136, T137), T138, T139) → U5_ggga(flattenB_in_ggga(T136, T137, cons(T138, T139)))
U6_ggga(flattenB_out_ggga(X85)) → flattenC_out_ggga(X85)
U3_ggga(T78, T89, flattenA_out_ga(X131)) → flattenB_out_ggga(.(T78, .(T89, X131)))
U4_ggga(T78, flattenB_out_ggga(X192)) → flattenB_out_ggga(.(T78, X192))
U5_ggga(flattenB_out_ggga(X209)) → flattenB_out_ggga(X209)
flattenA_in_ga(atom(T97)) → flattenA_out_ga(.(T97, []))
flattenA_in_ga(cons(atom(T106), T107)) → U1_ga(T106, flattenA_in_ga(T107))
flattenA_in_ga(cons(cons(T116, T117), T118)) → U2_ga(flattenB_in_ggga(T116, T117, T118))
U1_ga(T106, flattenA_out_ga(X158)) → flattenA_out_ga(.(T106, X158))
U2_ga(flattenB_out_ggga(X175)) → flattenA_out_ga(X175)
flattenC_in_ggga(x0, x1, x2)
flattenB_in_ggga(x0, x1, x2)
U6_ggga(x0)
U3_ggga(x0, x1, x2)
U4_ggga(x0, x1)
U5_ggga(x0)
flattenA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0)
The following rules are removed from R:
COUNTD_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → U9_GA(flattenC_in_ggga(T51, T52, T53))
U9_GA(flattenC_out_ggga(T56)) → COUNTD_IN_GA(T56)
COUNTD_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTD_IN_GA(T30)
COUNTD_IN_GA(cons(cons(T157, T158), T159)) → U12_GA(flattenB_in_ggga(T157, T158, T159))
U12_GA(flattenB_out_ggga(T160)) → COUNTD_IN_GA(T160)
Used ordering: POLO with Polynomial interpretation [POLO]:
flattenB_in_ggga(atom(T78), atom(T89), T90) → U3_ggga(T78, T89, flattenA_in_ga(T90))
flattenB_in_ggga(atom(T78), cons(T125, T126), T127) → U4_ggga(T78, flattenB_in_ggga(T125, T126, T127))
U6_ggga(flattenB_out_ggga(X85)) → flattenC_out_ggga(X85)
U4_ggga(T78, flattenB_out_ggga(X192)) → flattenB_out_ggga(.(T78, X192))
flattenA_in_ga(atom(T97)) → flattenA_out_ga(.(T97, []))
flattenA_in_ga(cons(atom(T106), T107)) → U1_ga(T106, flattenA_in_ga(T107))
flattenA_in_ga(cons(cons(T116, T117), T118)) → U2_ga(flattenB_in_ggga(T116, T117, T118))
U1_ga(T106, flattenA_out_ga(X158)) → flattenA_out_ga(.(T106, X158))
U2_ga(flattenB_out_ggga(X175)) → flattenA_out_ga(X175)
POL(.(x1, x2)) = x1 + x2
POL(COUNTD_IN_GA(x1)) = 2·x1
POL(U12_GA(x1)) = 2 + 2·x1
POL(U1_ga(x1, x2)) = 1 + 2·x1 + x2
POL(U2_ga(x1)) = 1 + x1
POL(U3_ggga(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U4_ggga(x1, x2)) = 1 + 2·x1 + x2
POL(U5_ggga(x1)) = x1
POL(U6_ggga(x1)) = 2 + x1
POL(U9_GA(x1)) = 1 + 2·x1
POL([]) = 0
POL(atom(x1)) = 2 + 2·x1
POL(cons(x1, x2)) = 2 + x1 + x2
POL(flattenA_in_ga(x1)) = x1
POL(flattenA_out_ga(x1)) = x1
POL(flattenB_in_ggga(x1, x2, x3)) = x1 + x2 + x3
POL(flattenB_out_ggga(x1)) = x1
POL(flattenC_in_ggga(x1, x2, x3)) = 2 + x1 + x2 + x3
POL(flattenC_out_ggga(x1)) = 1 + x1
flattenB_in_ggga(cons(T136, T137), T138, T139) → U5_ggga(flattenB_in_ggga(T136, T137, cons(T138, T139)))
U5_ggga(flattenB_out_ggga(X209)) → flattenB_out_ggga(X209)
U3_ggga(T78, T89, flattenA_out_ga(X131)) → flattenB_out_ggga(.(T78, .(T89, X131)))
flattenC_in_ggga(T63, T64, T65) → U6_ggga(flattenB_in_ggga(T63, T64, T65))
flattenC_in_ggga(x0, x1, x2)
flattenB_in_ggga(x0, x1, x2)
U6_ggga(x0)
U3_ggga(x0, x1, x2)
U4_ggga(x0, x1)
U5_ggga(x0)
flattenA_in_ga(x0)
U1_ga(x0, x1)
U2_ga(x0)